$\forall$$R$:es\_realizer\{i:l\}, $y$,$i$:Id. ($\uparrow$read{-}restricted($R$; $i$; $y$)) $\Rightarrow$ ($\uparrow$R{-}has{-}loc($R$; $i$))